COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	oppen[f81,jmc]		making Oppen's decision procedure useful
C00005 ENDMK
C⊗;
oppen[f81,jmc]		making Oppen's decision procedure useful

	Derek Oppen published a decision procedure for the first order
theory of car, cdr, cons, atom and equality.  No other functions are
allowed.  Adjoining the recursive definition of  istail  makes the theory
equivalent to Peano arithmetic.  The matter is somewhat discussed in
Cartwright and McCarthy (1978).

	We could imagine putting this decision procedure into EKL, but
problems in this pure theory don't seem to arise naturally.  However,
we may get something useful according to the following considerations.

	1. The theory can be extended to an arbitrary number of
constructors and selectors and the decision procedure still works.
Namely a new constructor  foo  of (say) three arguments can be
regarded as defined by

	foo(x,y,z) = cons(FOO,cons(x,cons(y,cons(z,NIL))))

where  FOO  is a constant not previously used.  In order to avoid
conflicts with formulas that are writable in the language with  foo
and  cons, we may need to define a new  cons  by

	cons1(x,y) = cons(CONS,cons(x,cons(y,NIL))).

	The selectors associated with  foo  and friends become
compositions of  car  and  cdr.

	2. Oppen's proof requires that distinct compositions of the
constructors result in distinct objects.

	3. We can suppose that situations arise in which some collection
of available functions have this property.  Then Oppen's decision
procedure works even if still other available functions have still other
properties.

	4. Moreover, the validity of some formulas that might be proved
don't depend on the functions having these properties.